"""
This is an implementation of untyped lambda calculus using Higher Order
Abstract Syntax (HOAS). It demonstrates how we can look inside lambda functions
by passing them dummy objects like variable names.
"""


class Term:
    alphabet = set(['x', 'y', 'z', 'u', 'v', 'w'])
    

class Lam(Term):
    def __init__(self, body):
        self.body = body

    def __repr__(self):
        name = self.body.func_code.co_varnames[0]
        return "Lam(lambda %s: %r)" % (name, self.body(Dummy(name)))

    def __str__(self, paren=False, level=1, alphabet=Term.alphabet):
        # We can either use indexed names
        name = "x%d" % level
        # Or pick them from a predefined alphabet
        name = backup = alphabet.pop()
        # Or even retrieve the original variable name
        #name = self.body.func_code.co_varnames[0]
        s = "lam %s. %s" % (name, self.body(Dummy(name)).__str__(False, level + 1, alphabet))
        if paren:
            s = "(" + s + ")"
        alphabet.add(backup)
        return s

    def __call__(self, arg):
        # This is where substitution takes place.
        # We pass the argument to the Python lambda function.
        return self.body(arg)

    def evaluate(self):
        return Lam(self.body)


class App(Term):
    def __init__(self, left, right):
        self.left = left
        self.right = right

    def __repr__(self):
        return "App(%r, %r)" % (self.left, self.right)
    
    def __str__(self, paren=False, level=1, alphabet=Term.alphabet):
        return "%s %s" % (self.left.__str__(True, level, alphabet),
                          self.right.__str__(True, level, alphabet))

    def evaluate(self):
        return (self.left.evaluate())(self.right).evaluate()


class Dummy(str):
    """
    A Dummy class used to look inside lambda terms.
    """
    def __repr__(self):
        return str(self)
    
    def __str__(self, paren=False, level=1, alphabet=Term.alphabet):
        return str.__str__(self)


# Examples

I = Lam(lambda x : x)
K = Lam(lambda x : Lam (lambda y : x))
O = Lam(lambda x : App(x, x))

print "I = ", I
print "K = ", K
print "O = ", O

print "Evaluation examples:"
print App(I, I), " => ", App(I, I).evaluate()
print App(K, K), " => ", App(K, K).evaluate()
# The following loops forever
#print App(O, O), " => ", App(O, O).evaluate()
